/*******************************************************************\

Module: Goto Programs with Functions

Author: Daniel Kroening

Date: June 2003

\*******************************************************************/

#include <assert.h>

#include <base_type.h>
#include <std_code.h>

#include <map>
#include <sstream>

#include "goto_convert_functions.h"
#include "goto_inline.h"
#include "remove_skip.h"

#include <stdlib.h>
extern std::map<std::string, std::map<std::string, std::string> > struct_info;
extern std::map<std::string, std::map<std::string, int> > enum_info;
extern std::string i2string(int i);
/*******************************************************************\

Function: goto_convert_functionst::goto_convert_functionst

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

goto_convert_functionst::goto_convert_functionst(
  contextt &_context,
  const optionst &_options,
  goto_functionst &_functions,
  message_handlert &_message_handler):
  goto_convertt(_context, _options, _message_handler),
  functions(_functions)
{
}
  
/*******************************************************************\

Function: goto_convert_functionst::~goto_convert_functionst

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

goto_convert_functionst::~goto_convert_functionst()
{
}
/*******************************************************************\
generate map<string, string>
********************************************************************/
void GenerateMemberInformation(std::string s, std::map<std::string, std::string> &mem){
    int Flag1, Flag2;
    Flag1 = 0; Flag2 = 0;
    std::string s1, s2;
    std::stringstream ss (stringstream::in | stringstream::out);
    pair<std::string, std::string> p_mem;
    //std::cout << "s = " << s << std::endl;
    ss << s;
    while(ss >> s1){
        //std::cout << s1 << std::endl;
        if(Flag1 == 1){
            if(s1.compare("signedbv") == 0 || s1.compare("unsignedbv") == 0){
                p_mem.second = s1;
                Flag1 = 0;
            }
            else if(s1.compare("symbol") == 0){
                ss >> s1; ss >> s1; ss >> s1;
                s2 = s1.substr(7);
                p_mem.second = s2;
                Flag1 = 0;
            }
        }
        if(Flag2 == 1){
            if(s1.compare(0,1,"$") != 0){
                //std::cout << "s1 = " << s1 << std::endl;//quakeian
                p_mem.first = s1;
                Flag2 = 0;
                mem.insert(p_mem);
            }
            else{
                Flag2 = 0;
            }
        }
        if(s1.compare("type:") == 0){ Flag1 = 1; }
        if(s1.compare("name:") == 0){ Flag2 = 1; }
    }
    //test
    /*map<std::string, std::string>::iterator it;
    for(it = mem.begin(); it != mem.end(); it++){
        std::cout << (*it).first << " => " << (*it).second << std::endl;
    }*/
}
/*******************************************************************\
change string 2 int
********************************************************************/
int string2int(string s){
    int result = 0;
    int flag = 0;
    if(s[0]=='-'){ s.erase(0,1); flag= 1; }
    for(unsigned i1 = 0; i1 < s.size(); i1++){
        int ten = 1;
        for(unsigned i2 = 0; i2 < s.size()-i1-1; i2++){
            ten = ten * 10;
        }
        int d = (s[i1]-48)*ten;
        result = result + d;
    }
    if(flag == 1){ result = result * (-1); }
    return result;
}

/*******************************************************************\

Function: goto_convert_functionst::goto_convert

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

void goto_convert_functionst::goto_convert()
{
  // warning! hash-table iterators are not stable

  typedef std::list<irep_idt> symbol_listt;
  //std::map<std::string, std::map<std::string, std::string> > struct_info;
  symbol_listt symbol_list;

  forall_symbols(it, context.symbols)
  {
    if(!it->second.is_type &&
       it->second.type.id()==ID_code){
      symbol_list.push_back(it->first);
        }//這邊把struct member訊息率掉
      //std::cout << "first : " << it->first << std::endl;
      //std::cout << "second : " << it->second << std::endl;
    if(it->second.type.id() == ID_struct){
      //std::cout << "first : " << it->first << std::endl;
      unsigned indent = 4;
      std::string struct_name = it->second.type.get_named_sub().begin()->second.pretty(indent+2,0);
      std::pair<std::string, std::map<std::string, std::string> > pair_struct_info;
      std::map<std::string, std::string> mem_info;
      std::string find_type;
      std::string get_mem;
      std::string mem_type;
      std::string mem_name;
      //std::cout << "struct_name = " << struct_name << endl;
      forall_named_irep(it1, it->second.type.get_named_sub()){
          if(it1 != it->second.type.get_named_sub().begin()){
              #ifdef USE_DSTRING
              find_type=it1->first.as_string();
              #else
              find_type=it1->first;
              #endif
              //std::cout << "find_type = " << find_type << std::endl;
              //if(find_type.compare("type") == 0){
              //    mem_type = it1->second.pretty(indent+2, 0);
              //    std::cout << "mem_type = " << mem_type << std::endl;
              //}
              get_mem = it1->second.pretty(indent+2, 0);
              //cout << "it1->second =  " << it1->second << endl;
              GenerateMemberInformation(get_mem, mem_info);
              //std::cout << "get_mem = " << get_mem << endl;
          }
      }
      pair_struct_info.first = struct_name;
      pair_struct_info.second = mem_info;
      struct_info.insert(pair_struct_info);
      //test
      /*std::cout << "test_struct" << std::endl;
      std::map<std::string, std::map<std::string, std::string> >::iterator itx;
      std::map<std::string, std::string>::iterator ity;
      for(itx = struct_info.begin(); itx != struct_info.end(); itx++){
          std::cout << itx->first << std::endl;
          for(ity = itx->second.begin(); ity != itx->second.end(); ity++){
              std::cout << ity->first << " => " << ity->second << std::endl;
          }
      }*/
      
      //std::cout << "second : " << it->second.type.pretty(4) << std::endl;
      //std::cout << "second name: " << it->second.name << std::endl;
      //std::cout << "second type: " << it->second.type.id() << std::endl;
      //std::cout << "second base_name: " << it->second.base_name << std::endl;
      //std::cout << "second pretty_name: " << it->second.pretty_name << std::endl;
    }
    /*if(it->second.type.id() == ID_enum){
        cout << "ID_enum " << endl;
    }*/
    if(it->second.type.id() == ID_c_enum){
        //cout << "ID_c_enum " << it->second.type.get_string("tag") << endl;
        map<string, int> ms;
        enum_info.insert(pair<string, map<string, int> >(it->second.type.get_string("tag"), ms) );
    }
    /*if(it->second.type.id() == ID_elements){
        cout << "ID_element " << it->second << endl;
    }*/
    int i3; i3 = 0;
    if(it->second.type.id() == ID_symbol){
        std::map<std::string, std::map<std::string, int> >::iterator itm_enum;
        for(itm_enum = enum_info.begin(); itm_enum != enum_info.end(); itm_enum++){
            if(it->second.value.type().get_string("tag") == itm_enum->first){
                string s_enum_element_name = it->second.name.as_string();
                pair<string, int> pp_enum;
                unsigned i1, i2;
                for(i1 = 0, i2 = 0; i1 < s_enum_element_name.size(); i1++){
                    if(i2 == 4){
                        break;
                    }
                    if(s_enum_element_name[i1] == ':'){
                        i2 = i2 + 1;
                    }
                }
                s_enum_element_name.erase(0, i1);
                pp_enum.second = string2int(it->second.value.get("value").as_string());
                pp_enum.first = s_enum_element_name;
                itm_enum->second.insert(pp_enum);
                //test
                /*std::map<std::string, std::map<std::string, int> >::iterator itm_test;
                for(itm_test = enum_info.begin(); itm_test != enum_info.end(); itm_test++){
                    std::map<string, int>::iterator itmm_test;
                    for(itmm_test=itm_test->second.begin(); itmm_test!=itm_test->second.end(); itmm_test++){
                        cout << "first = " << itm_test->first << " 2_1 = " << itmm_test->first << " 2_2 = " << itmm_test->second << " s = " << s_enum_element_name << endl;
                    }
                }*/

                break;
            }
        }
    }
  }
  
  for(symbol_listt::const_iterator
      it=symbol_list.begin();
      it!=symbol_list.end();
      it++)
  {
    convert_function(*it);
  }
  
  functions.compute_location_numbers();

  // this removes the parse tree of the bodies from memory
  #if 0
  Forall_symbols(it, context.symbols)
  {
    if(!it->second.is_type &&
       it->second.type.id()==ID_code &&
       it->second.value.is_not_nil())
      it->second.value=codet();
  }
  #endif
}

/*******************************************************************\

Function: goto_convert_functionst::hide

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

bool goto_convert_functionst::hide(const goto_programt &goto_program)
{
  for(goto_programt::instructionst::const_iterator
      i_it=goto_program.instructions.begin();
      i_it!=goto_program.instructions.end();
      i_it++)
  {
    for(goto_programt::instructiont::labelst::const_iterator
        l_it=i_it->labels.begin();
        l_it!=i_it->labels.end();
        l_it++)
    {
      if(*l_it=="__CPROVER_HIDE")
        return true;
    }
  }
  
  return false;
}

/*******************************************************************\

Function: goto_convert_functionst::add_return

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

void goto_convert_functionst::add_return(
  goto_functionst::goto_functiont &f,
  const locationt &location)
{
  if(!f.body.instructions.empty() &&
     f.body.instructions.back().is_return())
    return; // not needed, we have one already
    
  // see if we have an unconditional goto at the end
  if(!f.body.instructions.empty() &&
     f.body.instructions.back().is_goto() &&
     f.body.instructions.back().guard.is_true())
    return;

  goto_programt::targett t=f.body.add_instruction();
  t->make_return();
  t->code=code_returnt();
  t->location=location;

  exprt rhs=exprt(ID_sideeffect, f.type.return_type());
  rhs.set(ID_statement, ID_nondet);
  t->code.move_to_operands(rhs);
}

/*******************************************************************\

Function: goto_convert_functionst::convert_function

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

void goto_convert_functionst::convert_function(const irep_idt &identifier)
{
  const symbolt &symbol=ns.lookup(identifier);
  goto_functionst::goto_functiont &f=functions.function_map[identifier];
  
  // make tmp variables local to function
  tmp_symbol_prefix=id2string(symbol.name)+"::$tmp::";
  temporary_counter=0;
  
  f.type=to_code_type(symbol.type);
  f.body_available=symbol.value.is_not_nil();

  if(!f.body_available) return;
  
  if(symbol.value.id()!=ID_code)
  {
    err_location(symbol.value);
    throw "got invalid code for function `"+id2string(identifier)+"'";
  }
  
  const codet &code=to_code(symbol.value);
  
  locationt end_location;

  if(code.get_statement()==ID_block)
    end_location=static_cast<const locationt &>(
      code.find("#end_location"));
  else
    end_location.make_nil();

  targets=targetst();
  targets.return_set=true;
  targets.return_value=
    f.type.return_type().id()!=ID_empty &&
    f.type.return_type().id()!=ID_constructor &&
    f.type.return_type().id()!=ID_destructor;

  goto_convert_rec(code, f.body);
  
  // add non-det return value, if needed
  if(targets.return_value)
    add_return(f, end_location);
      
  // add "end of function"
  goto_programt::targett t=f.body.add_instruction();
  t->type=END_FUNCTION;
  t->location=end_location;
  t->code.set(ID_identifier, identifier);

  // do function tags
  Forall_goto_program_instructions(i_it, f.body)
    i_it->function=identifier;
  
  // remove_skip depends on the target numbers
  f.body.compute_target_numbers();

  remove_skip(f.body);

  f.body.update();

  if(hide(f.body))
    f.type.set("#hide", true);
}

/*******************************************************************\

Function: goto_convert

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

void goto_convert(
  contextt &context,
  const optionst &options,
  goto_functionst &functions,
  message_handlert &message_handler)
{
  goto_convert_functionst goto_convert_functions(
    context, options, functions, message_handler);
  
  try
  {  
    goto_convert_functions.goto_convert();
  }

  catch(int)
  {
    goto_convert_functions.error();
  }

  catch(const char *e)
  {
    goto_convert_functions.error(e);
  }

  catch(const std::string &e)
  {
    goto_convert_functions.error(e);
  }

  if(goto_convert_functions.get_error_found())
    throw 0;
}

/*******************************************************************\

Function: goto_convert

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

void goto_convert(
  const irep_idt &identifier,
  contextt &context,
  const optionst &options,
  goto_functionst &functions,
  message_handlert &message_handler)
{
  goto_convert_functionst goto_convert_functions(
    context, options, functions, message_handler);
  
  try
  {  
    goto_convert_functions.convert_function(identifier);
  }

  catch(int)
  {
    goto_convert_functions.error();
  }

  catch(const char *e)
  {
    goto_convert_functions.error(e);
  }

  catch(const std::string &e)
  {
    goto_convert_functions.error(e);
  }

  if(goto_convert_functions.get_error_found())
    throw 0;
}


